ltg:(IdLnkIdType), i:Id. (ltg  da-outlinks(;i))  False 

latex

Definitions	, da-outlinks(da;i), (x  l), da-outlink-f(da;k), fpf-dom-list(f), mapfilter(f;P;L), Prop, l[i], x:A. B(x), ||as||, IdLnk, Id, t  T, x:A. B(x), A & B, , AB, A, False, P  Q
Lemmas	Id wf, IdLnk wf, length wf2, select wf, nat wf